Nuprl Lemma : fifoReceiver-properties
11,40
postcript
pdf
es
:ES,
ff
:FIFO,
j
,
i
:
ff
.C,
e
:{
e
:E|
ff
.S(
j
,
i
,
e
)} .
ff
.Sender(
i
,
ff
.Receiver(
j
,
i
,
e
)) =
e
latex
Definitions
x
:
A
.
B
(
x
)
,
ff
.Receiver
,
t
T
,
,
t
.1
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
es-E
wf
,
fifoS
wf
,
fifoC
wf
,
FIFO
wf
,
event
system
wf
,
fifoR
wf
,
fifoSender
wf
origin
es:ES, ff:FIFO, j, i:ff.C, e:{e:E| ff.S(j,i,e)} . ff.Sender(i,ff.Receiver(j,i,e)) = e es:ES, ff:FIFO, j, i:ff.C, e:{e:E| ff.S(j,i,e)} . ff.Sender(i,ff.Receiver(j,i,e)) = e x:A. B(x)
T
x:A. B(x)
Q